Nuprl Lemma : update_wf
0,22
postcript
pdf
A
,
B
:Type,
eq
:(
A
A
),
f
:(
A
B
),
x
:
A
,
v
:
B
.
f
[
x
:=
v
]
A
B
latex
Definitions
f
[
x
:=
v
]
,
if
b
t
else
f
fi
,
x
:
A
.
B
(
x
)
,
,
t
T
Lemmas
bool
wf
,
ifthenelse
wf
origin
A, B:Type, eq:(A
A
), f:(AB), x:A, v:B. f[x:=v] 
AB A, B:Type, eq:(AA), f:(AB), x:A, v:B. f[x:=v] AB 
t else f fix:A. B(x) T